Nuprl Lemma : equiv_rel_self_functionality
13,42
postcript
pdf
T
:Type,
R
:(
T
T
).
EquivRel(
T
;
x
,
y
.
R
(
x
,
y
))
{
a
,
a'
,
b
,
b'
:
T
.
R
(
a
,
b
)
R
(
a'
,
b'
)
(
R
(
a
,
a'
)
R
(
b
,
b'
))}
latex
Up
rel
1
,
rel
1
Definitions
{
T
}
,
x
,
y
.
t
(
x
;
y
)
,
t
T
,
P
Q
,
P
&
Q
,
P
Q
,
x
(
s1
,
s2
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
Trans(
T
;
x
,
y
.
E
(
x
;
y
))
,
Sym(
T
;
x
,
y
.
E
(
x
;
y
))
,
Refl(
T
;
x
,
y
.
E
(
x
;
y
))
,
EquivRel(
T
;
x
,
y
.
E
(
x
;
y
))
Lemmas
equiv
rel
wf
origin
T:Type, R:(T
T
).
{a, a', b, b':T. R(a,b) R(a',b') (R(a,a') 
R(b,b'))} T:Type, R:(TT).
{a, a', b, b':T. R(a,b) R(a',b') (R(a,a') R(b,b'))} 
x,y. t(x;y)
T Q Q Qx:A. B(x)